|
Bunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. Sub-trees of the context tree are referred to as ''bunches''; hence the name. The internal nodes in the context tree are labelled with the mode of composition — multiplicative or additive, with the following characteristics: * Multiplicative composition denies the structural rules of weakening and contraction. * Additive composition admits weakening and contraction of entire bunches. Corresponding to each of these bunch combinators is conjunction, and each conjunction has an associated implication; hence the name, the logic of bunched implications. The semantics of bunched logic can be given in terms of Kripke models in which the set of worlds carries not only a preorder but also a monoidal product. Categorical models of bunched logic are given by doubly closed categories, which are both cartesian closed and symmetric monoidal closed. Day's tensor product construction can be used to generate categorical models corresponding to the Kripke semantics. Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP in order to give a logic which characterizes, in the sense of Hennessey-Milner, the compositional structure of concurrent systems. Bunched logic extended with a semantic model of locations and store is known as separation logic. It has been used to define the logic of pointer-analysis in languages like ALGOL or C. The implicational fragment of bunched logic has been given a games semantics. ==See also== * Linear logic 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Bunched logic」の詳細全文を読む スポンサード リンク
|